Issue3566-3.agda:14,8-11
(r₁ : R) → P (R.a r₁) !=< A
when checking that the expression R.b has type A
